Definitions | t T, x:A. B(x), E, ||as||, b, P  Q, False, A, A B, , [e, e'], l[i], pred(e), firstn(n;as), Prop,  b, , i= j, P & Q, P  Q, Unit, if b t else f fi, (e <loc e'), {T},  x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, 1of(t),  x,y. t(x;y), P Q, P  Q, e e' , i j < k, {i..j }, Top, S T, SQType(T), Trans x,y:T. E(x;y), True, T, hd(l), i< j, i j, as @ bs, Dec(P), first(e), i j, t ...$L |